OK. Hello everybody. We are looking at, if you think of it from an agent perspective,

logical based agents, where the world state is actually expressed in a world description

language, which could be many languages. We're going to look at essentially four of them. We

have looked at two, namely one is normal propositional logic and PLNQ. Those are the

same except that we give ourselves a little bit more leverage in writing down atomic propositions

in the PLNQ case. And we are in the part where we look at inference procedures. We have looked

at a couple of inference procedures. Calculi, the Hilbert calculus, which was horrible, not only

difficult for humans, but also very difficult for machines. We've looked at natural deduction,

which is kind of good for humans, but bad for machines. And we've looked at resolution and

tableau, which is good for machines, but not the best for propositional logic. I've introduced them

at the propositional level because they are going to be the dominant things in first-order logic and

so on. And the dominant procedure in propositional satisfiability checking is DPLL. Remember,

DPLL works the following way. One is if we have unit clauses, that's good because we can force

because unit clauses force a certain, if you want, decision in the truth value assignment.

And we can propagate that, essentially the same way we propagated it in constraint satisfaction.

And if we can't make progress because we don't have any units anymore, we resort to splitting.

Here we can see splitting happening. S is a variable that's currently unsolved or unassigned,

and then we just systematically search and look at both of these cases, either by making it true,

propagating, maybe making units and all of those kind of, or making it false, again propagating,

and maybe making more units. And these splitings actually let us make progress. But we have to

look at both possible cases and that makes the whole thing exponential, a search procedure.

This is extremely efficient in practice, partially also because the data structures you need to work

with are very easy to implement and you can optimize them very well. The procedure is

essentially a black box. If the formula is satisfiable, it gives you back an assignment,

that you can check. If it's unsatisfiable, you're out of luck because it just tells you

unsatisfiable. If you can get the procedure to give you the splitting tree, which is this thing

here, which is basically the trace of variables you've split on, which really is a tree only

that I didn't have space for it on the slide, and with all the clauses that are dangling for it,

then you can basically reinterpret this as a resolution proof. Essentially the splitting

variables tell you where to resolve. If you think about it, if you have those two here,

you can resolve on S, which is what this thing tells you, and the resulting clause will have

a Q literal. The splitting is actually resolutions between non-units, typically, and the remainder

simulating the unit propagation you can do via unit resolution. You can turn any trace

into a resolution proof, and that is again something you can check. Whenever in computer

science, logic, wherever, you have a procedure that tells you a yes and no answer, then it's

very hard typically to verify this. What we're very often interested in is algorithms that

can return a certificate. Here, this trace here, you could view as a certificate because you can,

in low order polynomial time, verify from that. The same thing if you have a prime factorization

procedure and it just says yes, this is not a prime, then you know nothing. If it gives you

the prime factors, you can just multiply them out, which is low order polynomial, and then you can

check the result. That's what we're seeing here. There's a question.

Well, this is kind of a trace of the ETPL algorithm, and this is an honest to goodness resolution proof.

Yes, so we are starting the DPLL up there, whereas you can think of this resolution proof

starts by resolving between those two clauses to get that. Yes, it goes up to the empty clause,

at which point we say hooray, we know it's unsatisfiable. The important thing is that normally you have a lot of

search and resolution theorem proving. Here, you do not have the search because the trace tells you what to do.

You just go through the motion. You don't derive all these clauses that are not going to contribute to the proof.

Okay, so if you look at it, then if we use this correspondence between resolution proofs and DPLL,

then one of the things you can see is that DPLL is tree resolution. What comes out are tree-shaped forms.

And we know that at least in more expressive logics, like the first logic, we are going to look at,